#!/usr/bin/env python3
import unittest

from z3 import *


class TestLogical(unittest.TestCase):
    def test_basic_bool(self):
        # 定义三个bool类型的变量，他们的值未确定
        p = Bool('p')
        q = Bool('q')
        r = Bool('r')
        # 求解约束
        # Implies(p, q)：表示逻辑蕴含"p→q"（如果p为真，则q必须为真）
        # r == Not(q)：表示r必须等于q的否定
        # Or(Not(p), r)：表示¬p∨r（p为假或者r为真）
        solve(Implies(p, q), r == Not(q), Or(Not(p), r))
        # 可能得值是[q = True, p = False, r = False]

    def test_basic_bool_and_pybol(self):
        p = Bool('p')
        q = Bool('q')
        # 直接输出
        print(And(p, q, True))
        # 简化And会把True省略，输出And(p, q)
        print(simplify(And(p, q, True)))
        print(simplify(And(p, False)))

    def test_mix(self):
        """
        John, Aries, and Joseph are brothers with different ages. Who is the youngest if the following statements are true?

        I. Aries is the oldest.
        II. John is not the youngest.
        """

        """
        Ages: 0 1 2
        """

        def min(li):
            m = li[0]
            for i in li[1:]:
                m = z3.If(i < m, i, m)
            return m

        def max(li):
            m = li[0]
            for i in li[1:]:
                m = z3.If(i > m, i, m)
            return m
        # 假设他们三个的年龄是三个整数
        john, aries, joseph = z3.Ints('john aries joseph')
        # 年龄数组
        bros = [john, aries, joseph]

        solver = z3.Solver()
        # 条件去重
        solver.add(z3.Distinct(bros))
        # 这三个年龄数字在0-2之间
        solver.add([z3.And(i >= 0, i <= 2) for i in bros])
        # 题目给的条件
        solver.add(aries == max(bros))
        solver.add(john != min(bros))

        if solver.check() == z3.sat:
            print(solver.model())
